T, T':Type, E:(TT), E':(T'T').
(T = T')
 (x, y:T. E(x,y)  E'(x,y))
 (EquivRel(T;x,y.E(x,y))  EquivRel(T';x,y.E'(x,y))) 

latex

ProofTree

Definitions	P  Q, P & Q, t  T, x(s1,s2), P  Q, P  Q, , x:A. B(x), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), EquivRel(T;x,y.E(x;y)), x. t(x), True, T, {T}, x(s)
Lemmas	iff wf, implies functionality wrt iff, all functionality wrt iff, and functionality wrt iff, iff functionality wrt iff, equiv rel iff, true wf, squash wf